\subsection{The Naive File System  \emph{$\mathtt{FS}$}}
\label{sec:Running-Naive}

\begin{figure}[t]%
	\begin{minipage}{\columnwidth}
		\begin{minipage}{0.41\columnwidth}
			\begin{footnotesize}
				\begin{tabular}{@{}c | @{}c@{} | c |@{}c@{}}
 					& Name & $\mathtt{SL}$ & $\mathtt{CR}$\\\hline\hline
					\multirow{3}{*}{\rotatebox{90}{Files}}
 					& $\mathtt{f1}$     &     2       & $\mathtt{NATO}$\\
 					& $\mathtt{f2}$     &     0       & $\mathtt{CIA}$\\
 					& $\mathtt{f3}$     &     1       & $\emptyset$\\\hline
					\multirow{3}{*}{\rotatebox{90}{Users}}
 					& $\mathtt{levi}$   &     3       & $\,\mathtt{NATO}, \mathtt{CIA}\,$\\
 					& $\mathtt{\,eugene\,}$ &     0       & $\,\mathtt{NATO}, \mathtt{CIA}\,$\\
				\end{tabular}
			\end{footnotesize}
		\end{minipage}%
		\hfill
		\begin{minipage}{0.50\columnwidth}
			\begin{tiny}
				\begin{ttfamily}
					\begin{tabular}{@{}r@{}l}
						M$_{_0}$(files)=& [file(f1, ac(s(s(ZERO)),\\
								   &	\phantom{M} list(NATO, empty)));\\
								   & file(f2, ac(ZERO,\\
								   & \phantom{M} list(CIA, empty)));\\
								   & file(f3, ac(s(ZERO),\\
								   & \phantom{M} empty))]\\
					 	M$_{_0}$(users)=& [user(levi, ac(s(s(s(ZERO))),\\
					 				& 	\phantom{M} list(NATO, list(CIA, empty)))));\\
					 				&  user(eugene, ac(ZERO,\\
					 				& 	\phantom{M} list(NATO, list(CIA, empty)))))]
					\end{tabular}				
				\end{ttfamily}
			\end{tiny}
		\end{minipage}
	\end{minipage}
	\caption{A simple \textsc{Fs} model and the corresponding initial marking.}%
	\label{fig:MLS-M}%
	
	\vspace{-0.4cm}
\end{figure}


A running example is used to illustrate the approach. It consists in a small \textsc{Dsl} representing a simplified version of an \textsc{Mls} File System. We first describe a possible metamodel describing the necessary data structures for representing File Systems, then the corresponding algebraic specification, and finally the behavioural semantics in terms of \textsc{Pn}s.

\subsubsection{An \textsc{Mls} File System Metamodel}
\label{sec:Running-Naive-MM}

Figure \ref{fig:MLS-MM} presents a simplified metamodel for \textsc{Mls} File Systems: it contains only files as objects and only users as subjects. A \textsf{File} and an \textsf{User} consists in a \textsf{name} and an associated \textsf{AccessClass}. An \textsf{AccessClass} is composed of an integer representing a \textsf{securityLevel} and a \textsf{Category} set. A \textsf{Category} is one of the following credential: \textsf{CIA}, \textsf{NATO} or \textsf{NUCLEAR} (represented as an enumeration). Access classes can be compared using the \textsf{dominates} operation: if $\mathsf{ac} = (\mathsf{s}, \mathsf{C})$ and $\mathsf{ac'} = (\mathsf{s'}, \mathsf{C'})$ are two access classes, where $\mathsf{s}, \mathsf{s'}\in \mathbb{N}$ represent security levels and $\mathsf{C}, \mathsf{C'}$ represent sets of credential categories, then $\mathsf{ac}$ \emph{dominates} $\mathsf{ac'}$ (noted $\mathsf{ac} \rhd \mathsf{ac'}$) iff  $\mathsf{ac}$ is ``\emph{stronger}'' than $\mathsf{ac'}$, \ie formally, if $\mathsf{s'}\leq \mathsf{s}$ and $\mathsf{C'} \subseteq \mathsf{C}$). 
Note that this notion of access class domination is different from the one classical in \textsc{Pn}, which operates on markings.

Consider now an \textsc{Mls} \textsc{Fs} model corresponding to the naive \textsc{Fs}, as described in \Fig \ref{fig:MLS-M}: it consists in three files and two users ($\mathtt{SL}$ stands for security level and $\mathtt{CR}$ for credential). Here, the user $\mathtt{levi}$ dominates all files whereas $\mathtt{eugene}$ only dominates file $\mathtt{f2}$. 

For now, any \textsc{Mls Fs} model (like the one depicted in \Fig \ref{fig:MLS-M}, left) conforming to the metamodel of \Fig \ref{fig:MLS-MM} is translated by hand in two steps into an \textsc{Apn}: 
\begin{itemize}
	\item the first step consists of a translation of the data structures specified by the metamodel into Abstract Data Types (\textsc{Adt}s); 
	\item the second step takes care of the behavioural semantics.
\end{itemize}
We detail each step in the following sections, providing an overview of how the translation is operated, giving further information about how to automatise it.


\subsubsection{Algebraic Data Types (\textsc{Adt}s)}
\label{sec:Running-Naive-ADT}


Classes \textsf{File} and \textsf{User} both contains an attribute \textsf{name} used to identify a file / user. Instead of using \textsf{string}, they are translated into sorts: all we really need is a way to compare such identifiers. In \Alpina, we use \textsf{Generators} to specify the initial marking (as described in \Fig \ref{fig:MLS-M} (left).

\smallskip
\begin{minipage}{\columnwidth}
	\begin{minipage}[b]{0.4\columnwidth}
		\setlistings{ADTlanguage}{0}
		\begin{lstlisting}{0}
Adt FileName
	Sorts fileName;
	Generators
		f1 : fileName;
		f2 : fileName;
		f3 : fileName;
		\end{lstlisting}
	\end{minipage}
	\hspace{0.5cm}
	\begin{minipage}[b]{0.45\columnwidth}
		\setlistings{ADTlanguage}{0}
		\begin{lstlisting}{0}
Adt UserName
	Sorts userName;
	Generators
		levi   : userName;
		eugene : userName;
		\end{lstlisting}
	\end{minipage}
\end{minipage}
This sorts are then used for creating sorts \textsf{file} and \textsf{user} following the same schema. First, a \textsf{generator} is defined for building a term of each sort, by combining a \textsf{name} with an \textsf{accessClass}. Then, two operations \textsf{name} and \textsf{class} return respectively the name and the class of such a term with the help of \textsf{variable}s prefixed in \Alpina with \textsf{\$}.

\smallskip\noindent
\begin{minipage}{\columnwidth}
	\begin{minipage}[b]{0.45\columnwidth}
		\setlistings{ADTlanguage}{0}
		\begin{lstlisting}{0}
import "fileName.adt"
import "accessClass.adt"
Adt File
	Sorts file;
	Generators
		file: fileName,accessClass->file;
	Operations
		name: file -> fileName;
		class: file -> accessClass;
	Axioms
		name(file($fn,$acl)) = $fn;
		class(file($fn,$acl)) = $acl;
	Variables
		fn  : fileName;
		acl : accessClass;
		\end{lstlisting}
	\end{minipage}
	\hspace{0.3cm}
	\begin{minipage}[b]{0.45\columnwidth}
		\setlistings{ADTlanguage}{0}
		\begin{lstlisting}{0}
import "userName.adt"
import "accessClass.adt"
Adt User
	Sorts user;
	Generators
		user: userName,accessClass->user;
	Operations
		name: user -> userName;
		class: user -> accessClass;
	Axioms
		name(user($un,$acl))  = $un;
		class(user($un,$acl)) = $acl;
	Variables
		un  : userName;
		acl : accessClass;
		\end{lstlisting}
	\end{minipage}
\end{minipage}
The enumeration \textsf{Category} is translated into a sort containing only three elements. An \textsc{Adt} \textsf{CategorySet} is defined to take care of the attribute \textsf{categorySet} in \textsf{AccessClass}: it makes use of the predefined generic \textsc{Adt} \textsf{List}, and contains only one operation \textsf{subset} for checking the access class' domination.

\smallskip\noindent
\begin{minipage}{\columnwidth}
	\begin{minipage}[b]{0.28\columnwidth}
		\setlistings{ADTlanguage}{0}
		\begin{lstlisting}{0}
Adt Category
	Sorts category;
	Generators
		NATO    : category;
		CIA     : category;
		NUCLEAR : category;
		\end{lstlisting}
	\end{minipage}
		\hspace{0.3cm}
	\begin{minipage}[b]{0.62\columnwidth}
		\setlistings{ADTlanguage}{0}
		\begin{lstlisting}{0}
import "boolean.adt"
import "category.adt"
import "list.gadt"
Adt CategorySet Is List[category]
	Operations
		subset : list[category], list[category] -> bool;
	Axioms
		empty subset $l = true;
		if contains($h,$l) = false then 
			list($h,$t) subset $l = false;	
		if contains($h,$l) = true then 
			list($h,$t) subset $l = $t subset $l;	
	Variables
		h : category;
		t : list[category];
		l : list[category];
		\end{lstlisting}
	\end{minipage}
\end{minipage}
In the class \textsf{AccessClass}, the attribute \textsf{securityLevel} is an \textsf{Integer} on which only an order is necessary for comparison. Therefore, it is encoded using a Peano-like sort representation, with $\mathtt{ZERO}$ for $0$ and $\mathtt{s}$ for the successor operation.

\noindent
\begin{center}
	\begin{minipage}[b]{0.52\columnwidth}
		\setlistings{ADTlanguage}{0}
		\begin{lstlisting}{0}
import "boolean.adt"
Adt securityLevel
	Sorts securityLevel;
	Generators
		ZERO: securityLevel;
		s: securityLevel -> securityLevel;		
	Operations
		le: securityLevel,securityLevel -> bool;
	Axioms
		ZERO le ZERO = true;
		ZERO le s($x) = true;		
		s($x) le ZERO = false;		
		s($x) le s($y) = $x le $y;
	Variables
		x : securityLevel;
		y : securityLevel;
		\end{lstlisting}
	\end{minipage}
\end{center}
Now, only the \textsf{AccessClass} class needs to be translated into an \textsc{Adt}. A generator \textsf{ac} is defined to build \textsf{accessClass}'s terms from terms of \textsf{securityLevel} and  \textsf{Category} list. Then, the \textsf{dominates} operation is defined according to the specification of \Sect \ref{sec:Running-Naive-ADT}.

\noindent
\begin{center}
	\begin{minipage}[b]{0.67\columnwidth}
		\setlistings{ADTlanguage}{0}
		\begin{lstlisting}{0}
import "boolean.adt"
import "categorySet.adt"
import "securityLevel.adt"
import "list.gadt"
import "category.adt"
Adt accessClass is list[category]
	Sorts accessClass;
	Generators
		ac : securityLevel, CategorySet -> accessClass;
	Operations
		dominates : accessClass, accessClass -> bool;
	Axioms
		if ($s2 le $s1)=true & ($c2 subset $c1)=true then 
			ac($s1,$c1) dominates ac($s2,$c2)= true;
		if ($s2 le $s1)=false & ($c2 subset $c1)=true then 
			ac($s1,$c1) dominates ac($s2,$c2)=false;
		if ($s2 le $s1)=true & ($c2 subset $c1)=false then 
			ac($s1,$c1) dominates ac($s2,$c2)=false;
		if ($s2 le $s1)=false & ($c2 subset $c1)=false then 
			ac($s1,$c1) dominates ac($s2,$c2)=false;		
	Variables
		s1 : securityLevel;
		s2 : securityLevel;
		c1 : CategorySet;
		c2 : CategorySet;
		\end{lstlisting}
	\end{minipage}
\end{center}
An extra \textsc{Adt} is defined for the purpose of the behavioural semantics. Named \textsf{FileUserPair}, it uses the generic \textsc{Adt} \textsf{Pair} to build a pair with a file and an user, and introduces an operation \textsf{userHasPermissionForFile} that checks if the user's access class dominates the file's access class.

\noindent
\begin{center}
	\begin{minipage}[b]{0.67\columnwidth}
		\setlistings{ADTlanguage}{0}
		\begin{lstlisting}{0}
import "boolean.adt"
import "pair.gadt"
import "file.adt"
import "user.adt"
Adt FileUserPair is pair[file,user]
	Operations
		userHasPermissionForFile : pair[file,user] -> bool;
	Axioms
		userHasPermissionForFile(pair($f,$u)) = 
			getAccessClass($u) dominates getAccessClass($f);
	Variables
		f : file;
		u : user;
		\end{lstlisting}
	\end{minipage}
\end{center}

\subsubsection{Behavioural Semantics}
\label{sec:Running-Naive-BS}




In the second step, we define the naive translational semantics of \textsc{Mls} systems \ie opening/closing files without credential checkings. The resulting \textsc{Apn} contains four places and four transitions. Places $\mathtt{files}$ and $\mathtt{users}$ contain files and users tokens, representing respectively the files and users objects corresponding to the initial marking of \Fig \ref{fig:MLS-M}. When an user wants to read or write a file, the corresponding transition ($\mathtt{openR}$ or $\mathtt{openW}$, respectively) is fired and consumes tokens $\mathtt{\$f}$ from place \textsf{files} and $\mathtt{\$u}$ from place $\mathtt{users}$; then produces a pair $\mathtt{\$p} = (\mathtt{\$f}, \mathtt{\$u})$ stored in the corresponding place. When $\mathtt{\$u}$ closes $\mathtt{\$f}$, the corresponding $\mathtt{close}$ transition is fired, which checks that $\mathtt{\$f}$ was actually opened by the user that opened it, and produces back tokens $\mathtt{\$f}$ and $\mathtt{\$u}$ into their respective places. Consuming file tokens every time a file is opened prevents another user from opening the same file.

Figure \ref{fig:naivefs} depicts the \textsc{Pn} that corresponds to the naive \textsc{Fs}. The marking of places $\mathtt{reading}$ and $\mathtt{writing}$ is empty (and denoted by empty brackets \texttt{[]}, and the marking for the two other places follows the initial marking of \Fig \ref{fig:MLS-M} (right). 
\begin{figure}[!htpb]
	\centering
	\epsfig{file=images/naive_fs, width=\linewidth}
	\caption{The naive File System $\FS$ with its initial marking $\mathtt{M}$.}
	\label{fig:naivefs}
	
	\vspace{-0.6cm}
\end{figure}
